| Definitions | left+right, P  Q, Knd, t  T, Top,   x. t(x),  x:A. B(x), a:A fp B(a), Type, x.A(x), "$x", Id, P   Q, ecl-machine3(ds;da;x;T;ks;a;snd), R-da(R;i), x:A B(x), ecl-machine2(i;ds;da;x;T;ks;a;upd), KindDeq, x dom(f),  b, Prop, , IdDeq, f || g, R-state-var(i;ds;da;x;T;ks;tr), x:A B(x), type List, (x l), {x:A| B(x) }, EqDecider(T),  , Atom$n, rec(x.A(x)), ecl(ds;da), msg-spec(ds;da), update-spec(ds;da), update-spec-decl(upd;ds),  A, fpf-domain(f), f  g, P  Q, P & Q, P Q, {T}, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, ecl-trans-ks(v), ecl-trans-tuple{i:l}(ds;da), ecl-trans(x), s = t, R-state-var-init(i;ds;da;x;T;v;ks;tr), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, True,  T, False, es realizer ind Reffect compseq tag def, Void,  x:A. B(x), S  T, es realizer ind Rframe compseq tag def, update-spec-vars(upd), Valtype(da;k), x : v, a = b, if b t else f fi, reduce(f;k;as), p q, <a,b>, car.cdr, b, SQType(T), s ~ t, Dec(P), IdLnk, msg-spec-links(snd), IdLnkDeq, remove-repeats(eq;L), dt(l;da), lnk-decl(l;dt), f(x)?z, source(l), t ...$L, ecl-tags(l;snd), f(a), x(s), A & B, tag(k), lnk(k), rcv(l,tg) |
| Lemmas | es-dt-dom, member-fpf-domain, rcv wf, lnk-decl-dom2, lnk wf, tagof wf, Knd sq, IdLnk sq, isrcv-implies, lnk-decl-dom-implies, R-lnk-tags-da, ecl-tags wf, lsrc wf, fpf-cap wf, lnk-decl wf, es-dt wf, remove-repeats wf, idlnk-deq wf, msg-spec-links wf, IdLnk wf, decidable l member, decidable equal Kind, bool cases, eqtt to assert, bool sq, eqff to assert, assert of bnot, not functionality wrt iff, assert-eq-id, fpf-single-dom, bool wf, bnot wf, cons member, fpf-empty-join, false wf, fpf-join-dom-sq, assert of bor, bor wf, reduce wf, ifthenelse wf, eq id wf, fpf-single wf, ma-valtype wf, update-spec-vars wf, R-da-Rall, R-state-var-da-dom, ecl-machine wf, not wf, update-spec-decl wf, update-spec wf, msg-spec wf, ecl wf, squash wf, true wf, ecl-kinds-ecl-trans, ecl-trans wf, ecl-trans-tuple wf, implies functionality wrt iff, iff transitivity, or functionality wrt iff, fpf-join-dom, fpf-join wf, l member wf, fpf-domain wf, subtype rel self, deq wf, R-state-var wf, fpf-compatible-symmetry, fpf-compatible-single, id-deq wf, Id wf, fpf-empty wf, assert wf, fpf-dom wf, Kind-deq wf, ecl-machine2 wf, fpf-trivial-subtype-top, R-da wf, ecl-machine3 wf, fpf wf, top wf, Knd wf |
upd:update-spec(ds;da).